Specification decimal-simple-ops

[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

enrich
   decimal
with
   

   
   constants  0_dec : decimal;
              1_dec : decimal;
   functions  . + . : decimal × decimal → decimal;
              . - . : decimal × decimal → decimal prio 8 left;
              . * . : decimal × decimal → decimal prio 10 right;
              ~ . : decimal → decimal;
              abs : decimal → decimal;
   predicates  . < . : decimal × decimal;
               . ≤ . : decimal × decimal;
               . > . : decimal × decimal;
               . ≥ . : decimal × decimal;
   
   
   
   

   

   axioms zero-def :  ⊦ 0_dec = mkDecimal(0, 0);
          used for: s, ls;
          one-def :  ⊦ 1_dec = mkDecimal(1, 0);
          add-def :  ⊦ dec_i + dec_j = mkDecimal(dec_i.int * 10 ^ dec_j.scale + dec_j.int * 10 ^ dec_i.scale, dec_i.scale + dec_j.scale);
          sub-def :  ⊦ dec_i - dec_j = mkDecimal(dec_i.int * 10 ^ dec_j.scale - dec_j.int * 10 ^ dec_i.scale, dec_i.scale + dec_j.scale);
          mult-def :  ⊦ dec_i * dec_j = mkDecimal(dec_i.int * dec_j.int, dec_i.scale + dec_j.scale);
          neg-def :  ⊦ ~ dec_i = mkDecimal(~ dec_i.int, dec_i.scale);
          abs-def :  ⊦ abs(dec_i) = mkDecimal(abs(dec_i.int), dec_i.scale);
          ls-def :  ⊦ dec_i < dec_j ↔ (dec_i - dec_j).int < 0;
          le-def :  ⊦ dec_i ≤ dec_j ↔ ¬ dec_j < dec_i;
          gr-def :  ⊦ dec_i > dec_j ↔ dec_j < dec_i;
          used for: s, ls;
          ge-def :  ⊦ dec_i ≥ dec_j ↔ ¬ dec_i < dec_j;
          used for: s, ls;

   

   
end enrich